Nuprl Definition : ma-bframe
11,40
postcript
pdf
M
.bframe(
k
sends on
l
) ==
L
!= (
M
.2.2.2.2.2.2.2.2.2).1(
k
)
deq-member(IdLnkDeq;
l
;
L
)
latex
clarification:
M
.bframe(
k
sends on
l
)
== fpf-val(KindDeq; ((
M
.2.2.2.2.2.2.2.2.2).1);
k
;
k
,
L
.(
deq-member(IdLnkDeq;
l
;
L
)))
latex
Definitions
z
!=
f
(
x
)
P
(
a
;
z
)
,
KindDeq
,
t
.1
,
t
.2
,
b
,
deq-member(
eq
;
x
;
L
)
,
IdLnkDeq
FDL editor aliases
ma-bframe
origin